#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include <pthread.h>

#define CAPACIDAD 16

void *set_buffer_to(void *arg);
void yield(void);

/* las variables globales y compartidas */
int buffer[CAPACIDAD];
pthread_mutex_t mutex;


int main(int argc, char *argv[]) {

    pthread_t hilo0,hilo1;
    int val[2] = {4,8};
    int i = 0;

    for(i=0; i<CAPACIDAD; i++)

        buffer[i] = 0;


    pthread_mutex_init(&mutex, NULL);
    pthread_create(&hilo0, NULL, set_buffer_to, (void *)&val[0]);
    pthread_create(&hilo1, NULL, set_buffer_to, (void *)&val[1]);
    /* sonda que comprueba que el Inv siempre se cumpla */
    while(1) {

        yield();
        pthread_mutex_lock(&mutex); /* Inicio SC */
        /* Inv: { \forall i : buffer[i]=buffer[0] } */
        for (i=0; i<CAPACIDAD; i++) {

            assert(buffer[i]==buffer[0]);
            yield();

        }
        pthread_mutex_unlock(&mutex); /* Fin SC */

    }

}


/* pone todo el buffer en un valor */
void *set_buffer_to(void *arg) {

    int val=0, i=0;

    val = *(int *)arg;

    while(1) {

        yield();
        pthread_mutex_lock(&mutex); /* Inicio SC */
        for (i=0; i<CAPACIDAD; i++) {

            buffer[i] = val;
            yield();

        }
        pthread_mutex_unlock(&mutex);   /* Fin SC */
        yield();

    }

}


/* se entrega al planificador de manera probabilistica */
void yield(void) {

    if (rand()%2)

        sched_yield();

}